ds:x:Id fp Type, da:k:Knd fp Type, a:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  Valtype(da;kind(e)))
 (n:, e1, e2:{e:E| loc(e) = i }. action[[a n]][e1;e2]  ) 

latex

Definitions	x:A. B(x), P  Q, t  T, action[[a n]][e1;e2], x. t(x), Prop, Id, , x(s), Dec(P), P  Q
Lemmas	ecl-es-act wf, es-E wf, Id wf, es-loc wf, nat wf, es-valtype wf, ma-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, ecl wf, fpf wf, Knd wf, decidable wf, le wf, btrue wf, bfalse wf